perm filename LISP.AX[F76,JMC] blob
sn#249278 filedate 1976-11-23 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00004 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 DECLARE INDVAR X Y Z
C00003 00003 AXIOM CONS:
C00004 00004 AXIOM APPEND:
C00005 ENDMK
C⊗;
DECLARE INDVAR X Y Z;
DECLARE OPCONST CAR CDR 1 [R←700];
DECLARE OPCONST CONS 2;
DECLARE PREDCONST ATOM NULL 1 [R←700];
DECLARE OPCONST * 2 [INF];
DECLARE PREDPAR P 1;
DECLARE INDCONST NILL;
AXIOM CONS:
∀X Y.(CAR CONS(X,Y) = X)
∀X Y.(CDR CONS(X,Y) = Y)
∀X.(¬ATOM X ⊃ CONS(CAR X,CDR X) = X)
∀X Y.¬ATOM CONS(X,Y)
;;
AXIOM INDUCTION:
∀X.(ATOM X ∨ P(CAR X) ∧ P(CDR X) ⊃ P(X)) ⊃ ∀X.P(X)
∀X.(NULL X ∨ P(CDR X) ⊃ P(X)) ⊃ ∀X.P(X)
;;
AXIOM LIST:
¬NULL CONS(X,Y)
NULL NILL
ATOM NILL
;;
AXIOM NULL:
∀X.(NULL X ≡ X = NILL)
;;
AXIOM APPEND:
∀X Y.(X * Y = IF NULL X THEN Y ELSE CONS(CAR X, CDR X * Y))
;;